Dave is big. Dave is cold. Dave is kind. Dave is quiet. Dave is not red. Dave is white. Erin is big. Erin is not cold. Erin is kind. Erin is quiet. Erin is red. Erin is not round. Gary is cold. Gary is not red. Harry is quiet. Harry is not white. If Harry is cold then Harry is big. Cold, quiet people are white. All round people are white. Big people are white. If someone is cold then they are quiet. All white people are big.
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is not red.
("Dave" "is" "red" "-")
Dave is white.
("Dave" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is not cold.
("Erin" "is" "cold" "-")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is not round.
("Erin" "is" "round" "-")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is not red.
("Gary" "is" "red" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is not white.
("Harry" "is" "white" "-")
If Harry is cold then Harry is big.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "big" "+"))
Cold, quiet people are white.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
All round people are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
Big people are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
If someone is cold then they are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
All white people are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
Gary is cold.
True
1
proof
[(triple13)]
("Gary" "is" "cold" "+")
triple13
Erin is round.
False
1
inv-proof
[(triple12)]
("Erin" "is" "round" "+")
triple12
Erin is white.
True
2
proof
[(((triple7) -> rule4))]
("Erin" "is" "white" "+")
((triple7) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is not white.
False
2
inv-proof
[(((triple7) -> rule4))]
("Erin" "is" "white" "-")
((triple7) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Gary is white.
True
4
proof
[(((triple13 ((triple13) -> rule5)) -> rule2))]
("Gary" "is" "white" "+")
((triple13 ((triple13) -> (rule5 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not white.
False
4
inv-proof
[(((triple13 ((triple13) -> rule5)) -> rule2))]
("Gary" "is" "white" "-")
((triple13 ((triple13) -> (rule5 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Harry is not big.
Unknown
inv-rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "big" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Dave is big.[(triple1 OR ((triple6) -> rule6) OR ((((triple2 triple4) -> rule2)) -> rule6) OR ((((triple2 ((triple2) -> rule5)) -> rule2)) -> rule6))] Dave is cold.[(triple2)] Dave is kind.[(triple3)] Dave is not red.[(triple5)] Dave is quiet.[(triple4 OR ((triple2) -> rule5))] Dave is white.[(triple6 OR ((triple1) -> rule4) OR ((triple2 triple4) -> rule2) OR ((triple2 ((triple2) -> rule5)) -> rule2))] Erin is big.[(triple7)] Erin is kind.[(triple9)] Erin is not cold.[(triple8)] Erin is not round.[(triple12)] Erin is quiet.[(triple10)] Erin is red.[(triple11)] Gary is cold.[(triple13)] Gary is not red.[(triple14)] Harry is not white.[(triple16)] Harry is quiet.[(triple15)] @1: Erin is white.[(((triple7) -> rule4))] Gary is quiet.[(((triple13) -> rule5))] @2: Gary is white.[(((triple13 ((triple13) -> rule5)) -> rule2))] @3: Gary is big.[(((((triple13 ((triple13) -> rule5)) -> rule2)) -> rule6))]
Dave is big.
("Dave" "is" "big" "+")
triple1
((triple6) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((triple2 triple4) -> (rule2 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple2 ((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is not red.
("Dave" "is" "red" "-")
triple5
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
((triple2) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple6
((triple1) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple2 triple4) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple2 ((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
triple7
Erin is kind.
("Erin" "is" "kind" "+")
triple9
Erin is not cold.
("Erin" "is" "cold" "-")
triple8
Erin is not round.
("Erin" "is" "round" "-")
triple12
Erin is quiet.
("Erin" "is" "quiet" "+")
triple10
Erin is red.
("Erin" "is" "red" "+")
triple11
Gary is cold.
("Gary" "is" "cold" "+")
triple13
Gary is not red.
("Gary" "is" "red" "-")
triple14
Harry is not white.
("Harry" "is" "white" "-")
triple16
Harry is quiet.
("Harry" "is" "quiet" "+")
triple15
Erin is white.
("Erin" "is" "white" "+")
((triple7) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple13) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple13 ((triple13) -> (rule5 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((((triple13 ((triple13) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3