Charlie is big. Charlie is cold. Charlie is green. Charlie is kind. Charlie is smart. Charlie is not white. Dave is green. Dave is kind. Dave is round. Dave is smart. Dave is white. Erin is big. Erin is green. Erin is round. Harry is not big. Harry is cold. If something is white and cold then it is not green. Round things are green. If something is cold then it is round.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is not white.
("Charlie" "is" "white" "-")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is round.
("Erin" "is" "round" "+")
Harry is not big.
("Harry" "is" "big" "-")
Harry is cold.
("Harry" "is" "cold" "+")
If something is white and cold then it is not green.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "green" "-"))
Round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
If something is cold then it is round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
Charlie is green.
True
1
proof
[(triple3 OR ((((triple2) -> rule3)) -> rule2))]
("Charlie" "is" "green" "+")
triple3
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Dave is not white.
False
1
inv-proof
[(triple11)]
("Dave" "is" "white" "-")
triple11
Harry is round.
True
2
proof
[(((triple16) -> rule3))]
("Harry" "is" "round" "+")
((triple16) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not round.
False
2
inv-proof
[(((triple16) -> rule3))]
("Harry" "is" "round" "-")
((triple16) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
True
3
proof
[(((((triple16) -> rule3)) -> rule2))]
("Harry" "is" "green" "+")
((((triple16) -> (rule3 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not green.
False
3
inv-proof
[(((((triple16) -> rule3)) -> rule2))]
("Harry" "is" "green" "-")
((((triple16) -> (rule3 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Charlie is big.[(triple1)] Charlie is cold.[(triple2)] Charlie is green.[(triple3 OR ((((triple2) -> rule3)) -> rule2))] Charlie is kind.[(triple4)] Charlie is not white.[(triple6)] Charlie is smart.[(triple5)] Dave is green.[(triple7 OR ((triple9) -> rule2))] Dave is kind.[(triple8)] Dave is round.[(triple9)] Dave is smart.[(triple10)] Dave is white.[(triple11)] Erin is big.[(triple12)] Erin is green.[(triple13 OR ((triple14) -> rule2))] Erin is round.[(triple14)] Harry is cold.[(triple16)] Harry is not big.[(triple15)] @1: Charlie is round.[(((triple2) -> rule3))] Harry is round.[(((triple16) -> rule3))] @2: Harry is green.[(((((triple16) -> rule3)) -> rule2))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is not white.
("Charlie" "is" "white" "-")
triple6
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Dave is green.
("Dave" "is" "green" "+")
triple7
((triple9) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple8
Dave is round.
("Dave" "is" "round" "+")
triple9
Dave is smart.
("Dave" "is" "smart" "+")
triple10
Dave is white.
("Dave" "is" "white" "+")
triple11
Erin is big.
("Erin" "is" "big" "+")
triple12
Erin is green.
("Erin" "is" "green" "+")
triple13
((triple14) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple14
Harry is cold.
("Harry" "is" "cold" "+")
triple16
Harry is not big.
("Harry" "is" "big" "-")
triple15
Charlie is round.
("Charlie" "is" "round" "+")
((triple2) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple16) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((((triple16) -> (rule3 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2