Dave is big. Dave is blue. Dave is furry. Dave is kind. Dave is quiet. Dave is red. Dave is white. Erin is quiet. Fiona is furry. Harry is kind. Harry is red. Harry is white. If someone is white then they are quiet. If someone is blue and quiet then they are furry. All furry people are quiet. If Erin is kind then Erin is quiet. Red, white people are furry. If Fiona is big then Fiona is red. If someone is red then they are white. If someone is big then they are furry.
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is white then they are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
If someone is blue and quiet then they are furry.
((("someone" "is" "blue" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
All furry people are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If Erin is kind then Erin is quiet.
((("Erin" "is" "kind" "+")) -> ("Erin" "is" "quiet" "+"))
Red, white people are furry.
((("someone" "is" "red" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
If Fiona is big then Fiona is red.
((("Fiona" "is" "big" "+")) -> ("Fiona" "is" "red" "+"))
If someone is red then they are white.
((("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
If someone is big then they are furry.
((("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
Dave is big.
True
1
proof
[(triple1)]
("Dave" "is" "big" "+")
triple1
Dave is not big.
False
1
inv-proof
[(triple1)]
("Dave" "is" "big" "-")
triple1
Harry is furry.
True
3
proof
[(((triple11 triple12) -> rule5) OR ((triple11 ((triple11) -> rule7)) -> rule5))]
("Harry" "is" "furry" "+")
((triple11 triple12) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple11 ((triple11) -> (rule7 % int2))) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Fiona is not quiet.
False
2
inv-proof
[(((triple9) -> rule3))]
("Fiona" "is" "quiet" "-")
((triple9) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Erin is not white.
Unknown
inv-rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "white" "-")
Fiona is white.
Unknown
rconc
[@2: Fiona is white.[CWA. Example of deepest failure = (rule7 <- rule6 <- FAIL)]]
("Fiona" "is" "white" "+")
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
@0: Dave is big.[(triple1)] Dave is blue.[(triple2)] Dave is furry.[(triple3 OR ((triple1) -> rule8) OR ((triple2 triple5) -> rule2) OR ((triple6 triple7) -> rule5) OR ((triple2 ((triple7) -> rule1)) -> rule2) OR ((triple6 ((triple6) -> rule7)) -> rule5) OR ((triple2 ((((triple6) -> rule7)) -> rule1)) -> rule2))] Dave is kind.[(triple4)] Dave is quiet.[(triple5 OR ((triple3) -> rule3) OR ((triple7) -> rule1) OR ((((triple1) -> rule8)) -> rule3) OR ((((triple6) -> rule7)) -> rule1) OR ((((triple6 triple7) -> rule5)) -> rule3) OR ((((triple6 ((triple6) -> rule7)) -> rule5)) -> rule3))] Dave is red.[(triple6)] Dave is white.[(triple7 OR ((triple6) -> rule7))] Erin is quiet.[(triple8)] Fiona is furry.[(triple9)] Harry is kind.[(triple10)] Harry is red.[(triple11)] Harry is white.[(triple12 OR ((triple11) -> rule7))] @1: Fiona is quiet.[(((triple9) -> rule3))] Harry is furry.[(((triple11 triple12) -> rule5) OR ((triple11 ((triple11) -> rule7)) -> rule5))] Harry is quiet.[(((triple12) -> rule1) OR ((((triple11) -> rule7)) -> rule1) OR ((((triple11 triple12) -> rule5)) -> rule3) OR ((((triple11 ((triple11) -> rule7)) -> rule5)) -> rule3))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
((triple1) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple2 triple5) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple6 triple7) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple2 ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((triple6 ((triple6) -> (rule7 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((triple2 ((((triple6) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
((triple3) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple7) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple1) -> (rule8 % int2))) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((triple6) -> (rule7 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple6 triple7) -> (rule5 % int2))) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((triple6 ((triple6) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
triple6
Dave is white.
("Dave" "is" "white" "+")
triple7
((triple6) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple8
Fiona is furry.
("Fiona" "is" "furry" "+")
triple9
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is white.
("Harry" "is" "white" "+")
triple12
((triple11) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple9) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple11 triple12) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple11 ((triple11) -> (rule7 % int2))) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple12) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple11) -> (rule7 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple11 triple12) -> (rule5 % int2))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((triple11 ((triple11) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3