Dave is blue. Dave is green. Dave is nice. Dave is quiet. Dave is smart. Fiona is big. Fiona is furry. Fiona is green. Fiona is nice. Fiona is smart. Smart people are furry. Nice people are furry. Nice people are furry. All blue people are furry. All nice, green people are furry. Nice, green people are blue. If Dave is big and Dave is smart then Dave is blue. All big people are smart.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Smart people are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
Nice people are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
Nice people are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
All blue people are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
All nice, green people are furry.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
Nice, green people are blue.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If Dave is big and Dave is smart then Dave is blue.
((("Dave" "is" "big" "+") ("Dave" "is" "smart" "+")) -> ("Dave" "is" "blue" "+"))
All big people are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
Fiona is furry.
True
1
proof
[(triple7 OR ((triple10) -> rule1) OR ((triple9) -> rule2) OR ((triple9) -> rule3) OR ((triple9 triple8) -> rule5) OR ((((triple6) -> rule8)) -> rule1) OR ((((triple9 triple8) -> rule6)) -> rule4))]
("Fiona" "is" "furry" "+")
triple7
((triple10) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((triple9) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((triple9) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((triple9 triple8) -> (rule5 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((((triple6) -> (rule8 % int2))) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple9 triple8) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Dave is not smart.
False
1
inv-proof
[(triple5)]
("Dave" "is" "smart" "-")
triple5
Fiona is blue.
True
3
proof
[(((triple9 triple8) -> rule6))]
("Fiona" "is" "blue" "+")
((triple9 triple8) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is not blue.
False
3
inv-proof
[(((triple9 triple8) -> rule6))]
("Fiona" "is" "blue" "-")
((triple9 triple8) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Dave is blue.[(triple1 OR ((triple3 triple2) -> rule6))] Dave is green.[(triple2)] Dave is nice.[(triple3)] Dave is quiet.[(triple4)] Dave is smart.[(triple5)] Fiona is big.[(triple6)] Fiona is furry.[(triple7 OR ((triple10) -> rule1) OR ((triple9) -> rule2) OR ((triple9) -> rule3) OR ((triple9 triple8) -> rule5) OR ((((triple6) -> rule8)) -> rule1) OR ((((triple9 triple8) -> rule6)) -> rule4))] Fiona is green.[(triple8)] Fiona is nice.[(triple9)] Fiona is smart.[(triple10 OR ((triple6) -> rule8))] @1: Dave is furry.[(((triple1) -> rule4) OR ((triple3) -> rule2) OR ((triple3) -> rule3) OR ((triple5) -> rule1) OR ((triple3 triple2) -> rule5) OR ((((triple3 triple2) -> rule6)) -> rule4))] Fiona is blue.[(((triple9 triple8) -> rule6))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
((triple3 triple2) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Fiona is big.
("Fiona" "is" "big" "+")
triple6
Fiona is furry.
("Fiona" "is" "furry" "+")
triple7
((triple10) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((triple9) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((triple9) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((triple9 triple8) -> (rule5 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((((triple6) -> (rule8 % int2))) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple9 triple8) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
triple8
Fiona is nice.
("Fiona" "is" "nice" "+")
triple9
Fiona is smart.
("Fiona" "is" "smart" "+")
triple10
((triple6) -> (rule8 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple1) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple3) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple3) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple5) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple3 triple2) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple3 triple2) -> (rule6 % int2))) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple9 triple8) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1