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