Dave is cold. Dave is furry. Dave is kind. Dave is young. Fiona is blue. Fiona is cold. Fiona is white. Gary is furry. Gary is kind. Gary is young. If Dave is kind and Dave is young then Dave is nice. All young people are white. If Dave is cold then Dave is furry. All cold, white people are nice. If Dave is white then Dave is kind. Blue people are cold. All white, furry people are blue. If someone is nice then they are furry.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is young.
("Gary" "is" "young" "+")
If Dave is kind and Dave is young then Dave is nice.
((("Dave" "is" "kind" "+") ("Dave" "is" "young" "+")) -> ("Dave" "is" "nice" "+"))
All young people are white.
((("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
If Dave is cold then Dave is furry.
((("Dave" "is" "cold" "+")) -> ("Dave" "is" "furry" "+"))
All cold, white people are nice.
((("someone" "is" "cold" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
If Dave is white then Dave is kind.
((("Dave" "is" "white" "+")) -> ("Dave" "is" "kind" "+"))
Blue people are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
All white, furry people are blue.
((("someone" "is" "white" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
If someone is nice then they are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
Gary is young.
True
1
proof
[(triple10)]
("Gary" "is" "young" "+")
triple10
Fiona is not blue.
False
1
inv-proof
[(triple5 OR ((triple7 ((((triple6 triple7) -> rule4)) -> rule8)) -> rule7))]
("Fiona" "is" "blue" "-")
triple5
((triple7 ((((triple6 triple7) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Gary is white.
True
2
proof
[(((triple10) -> rule2))]
("Gary" "is" "white" "+")
((triple10) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not white.
False
2
inv-proof
[(((triple10) -> rule2))]
("Gary" "is" "white" "-")
((triple10) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Dave is blue.
True
4
proof
[(((((triple4) -> rule2) triple2) -> rule7) OR ((((triple4) -> rule2) ((triple1) -> rule3)) -> rule7) OR ((((triple4) -> rule2) ((((triple3 triple4) -> rule1)) -> rule8)) -> rule7) OR ((((triple4) -> rule2) ((((triple1 ((triple4) -> rule2)) -> rule4)) -> rule8)) -> rule7) OR ((((triple4) -> rule2) ((((((((triple4) -> rule2)) -> rule5) triple4) -> rule1)) -> rule8)) -> rule7))]
("Dave" "is" "blue" "+")
((((triple4) -> (rule2 % int2)) triple2) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple4) -> (rule2 % int3)) ((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((triple4) -> (rule2 % int4)) ((((triple3 triple4) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
((((triple4) -> (rule2 % int4)) ((((triple1 ((triple4) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
((((triple4) -> (rule2 % int5)) ((((((((triple4) -> (rule2 % int5))) -> (rule5 % int4)) triple4) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
int5
Dave is not blue.
False
4
inv-proof
[(((((triple4) -> rule2) triple2) -> rule7) OR ((((triple4) -> rule2) ((triple1) -> rule3)) -> rule7) OR ((((triple4) -> rule2) ((((triple3 triple4) -> rule1)) -> rule8)) -> rule7) OR ((((triple4) -> rule2) ((((triple1 ((triple4) -> rule2)) -> rule4)) -> rule8)) -> rule7) OR ((((triple4) -> rule2) ((((((((triple4) -> rule2)) -> rule5) triple4) -> rule1)) -> rule8)) -> rule7))]
("Dave" "is" "blue" "-")
((((triple4) -> (rule2 % int2)) triple2) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple4) -> (rule2 % int3)) ((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((triple4) -> (rule2 % int4)) ((((triple3 triple4) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
((((triple4) -> (rule2 % int4)) ((((triple1 ((triple4) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
((((triple4) -> (rule2 % int5)) ((((((((triple4) -> (rule2 % int5))) -> (rule5 % int4)) triple4) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
int5
Gary is cold.
True
5
proof
[(((((((triple10) -> rule2) triple8) -> rule7)) -> rule6))]
("Gary" "is" "cold" "+")
((((((triple10) -> (rule2 % int3)) triple8) -> (rule7 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is not cold.
False
5
inv-proof
[(((((((triple10) -> rule2) triple8) -> rule7)) -> rule6))]
("Gary" "is" "cold" "-")
((((((triple10) -> (rule2 % int3)) triple8) -> (rule7 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
@0: Dave is cold.[(triple1 OR ((((((triple4) -> rule2) triple2) -> rule7)) -> rule6) OR ((((((triple4) -> rule2) ((((triple3 triple4) -> rule1)) -> rule8)) -> rule7)) -> rule6) OR ((((((triple4) -> rule2) ((((((((triple4) -> rule2)) -> rule5) triple4) -> rule1)) -> rule8)) -> rule7)) -> rule6))] Dave is furry.[(triple2 OR ((triple1) -> rule3) OR ((((triple3 triple4) -> rule1)) -> rule8) OR ((((triple1 ((triple4) -> rule2)) -> rule4)) -> rule8) OR ((((((((triple4) -> rule2)) -> rule5) triple4) -> rule1)) -> rule8))] Dave is kind.[(triple3 OR ((((triple4) -> rule2)) -> rule5))] Dave is young.[(triple4)] Fiona is blue.[(triple5 OR ((triple7 ((((triple6 triple7) -> rule4)) -> rule8)) -> rule7))] Fiona is cold.[(triple6 OR ((triple5) -> rule6))] Fiona is white.[(triple7)] Gary is furry.[(triple8)] Gary is kind.[(triple9)] Gary is young.[(triple10)] @1: Dave is nice.[(((triple3 triple4) -> rule1) OR ((triple1 ((triple4) -> rule2)) -> rule4) OR ((((((triple4) -> rule2)) -> rule5) triple4) -> rule1) OR ((((((((triple4) -> rule2) triple2) -> rule7)) -> rule6) ((triple4) -> rule2)) -> rule4))] Dave is white.[(((triple4) -> rule2))] Fiona is nice.[(((triple6 triple7) -> rule4) OR ((((triple5) -> rule6) triple7) -> rule4))] Gary is white.[(((triple10) -> rule2))] @2: Dave is blue.[(((((triple4) -> rule2) triple2) -> rule7) OR ((((triple4) -> rule2) ((triple1) -> rule3)) -> rule7) OR ((((triple4) -> rule2) ((((triple3 triple4) -> rule1)) -> rule8)) -> rule7) OR ((((triple4) -> rule2) ((((triple1 ((triple4) -> rule2)) -> rule4)) -> rule8)) -> rule7) OR ((((triple4) -> rule2) ((((((((triple4) -> rule2)) -> rule5) triple4) -> rule1)) -> rule8)) -> rule7))] Fiona is furry.[(((((triple6 triple7) -> rule4)) -> rule8) OR ((((((triple5) -> rule6) triple7) -> rule4)) -> rule8))] Gary is blue.[(((((triple10) -> rule2) triple8) -> rule7))] @3: Gary is cold.[(((((((triple10) -> rule2) triple8) -> rule7)) -> rule6))] @4: Gary is nice.[(((((((((triple10) -> rule2) triple8) -> rule7)) -> rule6) ((triple10) -> rule2)) -> rule4))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
((((((triple4) -> (rule2 % int3)) triple2) -> (rule7 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((((triple4) -> (rule2 % int5)) ((((triple3 triple4) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
int5
((((((triple4) -> (rule2 % int6)) ((((((((triple4) -> (rule2 % int6))) -> (rule5 % int5)) triple4) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
int5
Dave is white.
("Dave" "is" "white" "+")
int6
Dave is furry.
("Dave" "is" "furry" "+")
triple2
((triple1) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple3 triple4) -> (rule1 % int2))) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple1 ((triple4) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((((((triple4) -> (rule2 % int4))) -> (rule5 % int3)) triple4) -> (rule1 % int2))) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
triple3
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
triple4
Fiona is blue.
("Fiona" "is" "blue" "+")
triple5
((triple7 ((((triple6 triple7) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
triple6
((triple5) -> (rule6 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
triple7
Gary is furry.
("Gary" "is" "furry" "+")
triple8
Gary is kind.
("Gary" "is" "kind" "+")
triple9
Gary is young.
("Gary" "is" "young" "+")
triple10
Dave is nice.
("Dave" "is" "nice" "+")
((triple3 triple4) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple1 ((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((((triple4) -> (rule2 % int3))) -> (rule5 % int2)) triple4) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((((((triple4) -> (rule2 % int4)) triple2) -> (rule7 % int3))) -> (rule6 % int2)) ((triple4) -> (rule2 % int4))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
((triple4) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple6 triple7) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((((triple5) -> (rule6 % int2)) triple7) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((triple10) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((((triple4) -> (rule2 % int2)) triple2) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple4) -> (rule2 % int3)) ((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((triple4) -> (rule2 % int4)) ((((triple3 triple4) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
((((triple4) -> (rule2 % int4)) ((((triple1 ((triple4) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
((((triple4) -> (rule2 % int5)) ((((((((triple4) -> (rule2 % int5))) -> (rule5 % int4)) triple4) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
int5
Fiona is furry.
("Fiona" "is" "furry" "+")
((((triple6 triple7) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((((((triple5) -> (rule6 % int3)) triple7) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
((((triple10) -> (rule2 % int2)) triple8) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((((triple10) -> (rule2 % int3)) triple8) -> (rule7 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
((((((((triple10) -> (rule2 % int4)) triple8) -> (rule7 % int3))) -> (rule6 % int2)) ((triple10) -> (rule2 % int4))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4