Dave is blue. Dave is kind. Dave is round. Dave is smart. Dave is white. Fiona is cold. Fiona is round. Fiona is smart. Fiona is young. Harry is blue. Harry is smart. Harry is young. If Harry is young and Harry is cold then Harry is round. If something is smart and round then it is white. Young things are round. White, blue things are young. If something is kind and blue then it is round. All smart, kind things are white.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is young and Harry is cold then Harry is round.
((("Harry" "is" "young" "+") ("Harry" "is" "cold" "+")) -> ("Harry" "is" "round" "+"))
If something is smart and round then it is white.
((("something" "is" "smart" "+") ("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
Young things are round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
White, blue things are young.
((("something" "is" "white" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If something is kind and blue then it is round.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
All smart, kind things are white.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Fiona is cold.
True
1
proof
[(triple6)]
("Fiona" "is" "cold" "+")
triple6
Dave is not blue.
False
1
inv-proof
[(triple1)]
("Dave" "is" "blue" "-")
triple1
Dave is young.
True
3
proof
[(((triple5 triple1) -> rule4) OR ((((triple4 triple2) -> rule6) triple1) -> rule4) OR ((((triple4 triple3) -> rule2) triple1) -> rule4) OR ((((triple4 ((triple2 triple1) -> rule5)) -> rule2) triple1) -> rule4))]
("Dave" "is" "young" "+")
((triple5 triple1) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple4 triple2) -> (rule6 % int2)) triple1) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple4 triple3) -> (rule2 % int2)) triple1) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple4 ((triple2 triple1) -> (rule5 % int3))) -> (rule2 % int2)) triple1) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Harry is not round.
False
2
inv-proof
[(((triple12) -> rule3))]
("Harry" "is" "round" "-")
((triple12) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Dave is blue.[(triple1)] Dave is kind.[(triple2)] Dave is round.[(triple3 OR ((triple2 triple1) -> rule5) OR ((((triple5 triple1) -> rule4)) -> rule3) OR ((((((triple4 triple2) -> rule6) triple1) -> rule4)) -> rule3))] Dave is smart.[(triple4)] Dave is white.[(triple5 OR ((triple4 triple2) -> rule6) OR ((triple4 triple3) -> rule2) OR ((triple4 ((triple2 triple1) -> rule5)) -> rule2))] Fiona is cold.[(triple6)] Fiona is round.[(triple7 OR ((triple9) -> rule3))] Fiona is smart.[(triple8)] Fiona is young.[(triple9)] Harry is blue.[(triple10)] Harry is smart.[(triple11)] Harry is young.[(triple12)] @1: Dave is young.[(((triple5 triple1) -> rule4) OR ((((triple4 triple2) -> rule6) triple1) -> rule4) OR ((((triple4 triple3) -> rule2) triple1) -> rule4) OR ((((triple4 ((triple2 triple1) -> rule5)) -> rule2) triple1) -> rule4))] Fiona is white.[(((triple8 triple7) -> rule2) OR ((triple8 ((triple9) -> rule3)) -> rule2))] Harry is round.[(((triple12) -> rule3))] @2: Harry is white.[(((triple11 ((triple12) -> rule3)) -> rule2))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
((triple2 triple1) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple5 triple1) -> (rule4 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((((((triple4 triple2) -> (rule6 % int3)) triple1) -> (rule4 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
triple4
Dave is white.
("Dave" "is" "white" "+")
triple5
((triple4 triple2) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple4 triple3) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple4 ((triple2 triple1) -> (rule5 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
triple6
Fiona is round.
("Fiona" "is" "round" "+")
triple7
((triple9) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple8
Fiona is young.
("Fiona" "is" "young" "+")
triple9
Harry is blue.
("Harry" "is" "blue" "+")
triple10
Harry is smart.
("Harry" "is" "smart" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
Dave is young.
("Dave" "is" "young" "+")
((triple5 triple1) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple4 triple2) -> (rule6 % int2)) triple1) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple4 triple3) -> (rule2 % int2)) triple1) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple4 ((triple2 triple1) -> (rule5 % int3))) -> (rule2 % int2)) triple1) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
((triple8 triple7) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((triple8 ((triple9) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((triple12) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple11 ((triple12) -> (rule3 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2