Dave is big. Dave is quiet. Dave is smart. Fiona is furry. Fiona is kind. Fiona is red. Fiona is white. If Fiona is white then Fiona is smart. If something is smart then it is furry. If Dave is furry and Dave is smart then Dave is white. If Dave is red and Dave is kind then Dave is big. If something is smart then it is big. If Fiona is kind then Fiona is red.
Dave is big.
("Dave" "is" "big" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If Fiona is white then Fiona is smart.
((("Fiona" "is" "white" "+")) -> ("Fiona" "is" "smart" "+"))
If something is smart then it is furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
If Dave is furry and Dave is smart then Dave is white.
((("Dave" "is" "furry" "+") ("Dave" "is" "smart" "+")) -> ("Dave" "is" "white" "+"))
If Dave is red and Dave is kind then Dave is big.
((("Dave" "is" "red" "+") ("Dave" "is" "kind" "+")) -> ("Dave" "is" "big" "+"))
If something is smart then it is big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
If Fiona is kind then Fiona is red.
((("Fiona" "is" "kind" "+")) -> ("Fiona" "is" "red" "+"))
Dave is smart.
True
1
proof
[(triple3)]
("Dave" "is" "smart" "+")
triple3
Fiona is not white.
False
1
inv-proof
[(triple7)]
("Fiona" "is" "white" "-")
triple7
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Dave is big.[(triple1 OR ((triple3) -> rule5))] Dave is quiet.[(triple2)] Dave is smart.[(triple3)] Fiona is furry.[(triple4 OR ((((triple7) -> rule1)) -> rule2))] Fiona is kind.[(triple5)] Fiona is red.[(triple6 OR ((triple5) -> rule6))] Fiona is white.[(triple7)] @1: Dave is furry.[(((triple3) -> rule2))] Fiona is smart.[(((triple7) -> rule1))] @2: Dave is white.[(((((triple3) -> rule2) triple3) -> rule3))] Fiona is big.[(((((triple7) -> rule1)) -> rule5))]
Dave is big.
("Dave" "is" "big" "+")
triple1
((triple3) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Fiona is furry.
("Fiona" "is" "furry" "+")
triple4
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
triple5
Fiona is red.
("Fiona" "is" "red" "+")
triple6
((triple5) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
triple7
Dave is furry.
("Dave" "is" "furry" "+")
((triple3) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple7) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
((((triple7) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2