Bob is big. Bob is cold. Bob is green. Bob is kind. Bob is red. Bob is smart. Bob is young. Charlie is cold. Charlie is kind. Charlie is red. Charlie is smart. Charlie is young. Dave is cold. Dave is kind. Dave is young. Green things are red. If Dave is cold then Dave is red. If something is big then it is red. Cold, young things are kind. If Charlie is cold then Charlie is red. Kind, young things are smart. If something is red then it is green. Kind, young things are red.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is young.
("Dave" "is" "young" "+")
Green things are red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If Dave is cold then Dave is red.
((("Dave" "is" "cold" "+")) -> ("Dave" "is" "red" "+"))
If something is big then it is red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
Cold, young things are kind.
((("something" "is" "cold" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
If Charlie is cold then Charlie is red.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "red" "+"))
Kind, young things are smart.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
If something is red then it is green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
Kind, young things are red.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
Bob is young.
True
1
proof
[(triple7)]
("Bob" "is" "young" "+")
triple7
Dave is not cold.
False
1
inv-proof
[(triple13)]
("Dave" "is" "cold" "-")
triple13
Dave is red.
True
2
proof
[(((triple13) -> rule2) OR ((triple14 triple15) -> rule8) OR ((((triple13 triple15) -> rule4) triple15) -> rule8))]
("Dave" "is" "red" "+")
((triple13) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple14 triple15) -> (rule8 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple13 triple15) -> (rule4 % int2)) triple15) -> (rule8 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not red.
False
2
inv-proof
[(((triple13) -> rule2) OR ((triple14 triple15) -> rule8) OR ((((triple13 triple15) -> rule4) triple15) -> rule8))]
("Dave" "is" "red" "-")
((triple13) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple14 triple15) -> (rule8 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple13 triple15) -> (rule4 % int2)) triple15) -> (rule8 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Bob is big.[(triple1)] Bob is cold.[(triple2)] Bob is green.[(triple3 OR ((triple5) -> rule7) OR ((((triple1) -> rule3)) -> rule7) OR ((((triple4 triple7) -> rule8)) -> rule7) OR ((((((triple2 triple7) -> rule4) triple7) -> rule8)) -> rule7))] Bob is kind.[(triple4 OR ((triple2 triple7) -> rule4))] Bob is red.[(triple5 OR ((triple1) -> rule3) OR ((triple3) -> rule1) OR ((triple4 triple7) -> rule8) OR ((((triple2 triple7) -> rule4) triple7) -> rule8))] Bob is smart.[(triple6 OR ((triple4 triple7) -> rule6) OR ((((triple2 triple7) -> rule4) triple7) -> rule6))] Bob is young.[(triple7)] Charlie is cold.[(triple8)] Charlie is kind.[(triple9 OR ((triple8 triple12) -> rule4))] Charlie is red.[(triple10 OR ((triple8) -> rule5) OR ((triple9 triple12) -> rule8) OR ((((triple8 triple12) -> rule4) triple12) -> rule8))] Charlie is smart.[(triple11 OR ((triple9 triple12) -> rule6) OR ((((triple8 triple12) -> rule4) triple12) -> rule6))] Charlie is young.[(triple12)] Dave is cold.[(triple13)] Dave is kind.[(triple14 OR ((triple13 triple15) -> rule4))] Dave is young.[(triple15)] @1: Charlie is green.[(((triple10) -> rule7) OR ((((triple8) -> rule5)) -> rule7) OR ((((triple9 triple12) -> rule8)) -> rule7) OR ((((((triple8 triple12) -> rule4) triple12) -> rule8)) -> rule7))] Dave is red.[(((triple13) -> rule2) OR ((triple14 triple15) -> rule8) OR ((((triple13 triple15) -> rule4) triple15) -> rule8))] Dave is smart.[(((triple14 triple15) -> rule6) OR ((((triple13 triple15) -> rule4) triple15) -> rule6))] @2: Dave is green.[(((((triple13) -> rule2)) -> rule7) OR ((((triple14 triple15) -> rule8)) -> rule7) OR ((((((triple13 triple15) -> rule4) triple15) -> rule8)) -> rule7))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
((triple5) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((triple4 triple7) -> (rule8 % int2))) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((((triple2 triple7) -> (rule4 % int3)) triple7) -> (rule8 % int2))) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
triple4
((triple2 triple7) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple5
((triple1) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple3) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple4 triple7) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple2 triple7) -> (rule4 % int2)) triple7) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
triple6
((triple4 triple7) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple2 triple7) -> (rule4 % int2)) triple7) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
triple7
Charlie is cold.
("Charlie" "is" "cold" "+")
triple8
Charlie is kind.
("Charlie" "is" "kind" "+")
triple9
((triple8 triple12) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple10
((triple8) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple9 triple12) -> (rule8 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((triple8 triple12) -> (rule4 % int2)) triple12) -> (rule8 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple11
((triple9 triple12) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple8 triple12) -> (rule4 % int2)) triple12) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
triple12
Dave is cold.
("Dave" "is" "cold" "+")
triple13
Dave is kind.
("Dave" "is" "kind" "+")
triple14
((triple13 triple15) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple15
Charlie is green.
("Charlie" "is" "green" "+")
((triple10) -> (rule7 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((((triple8) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((triple9 triple12) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((((triple8 triple12) -> (rule4 % int3)) triple12) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
((triple13) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple14 triple15) -> (rule8 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple13 triple15) -> (rule4 % int2)) triple15) -> (rule8 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((triple14 triple15) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((((triple13 triple15) -> (rule4 % int2)) triple15) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((((triple13) -> (rule2 % int2))) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((triple14 triple15) -> (rule8 % int2))) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((((triple13 triple15) -> (rule4 % int3)) triple15) -> (rule8 % int2))) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3