Bob is rough. Bob is round. Bob is smart. Charlie is big. Charlie is quiet. Charlie is rough. Charlie is round. Charlie is smart. Gary is big. Gary is green. Gary is rough. Gary is round. Gary is smart. Harry is green. Harry is quiet. Rough, green things are quiet. If something is green then it is round. All smart things are kind. All rough, smart things are round. Quiet, rough things are smart. If something is rough and quiet then it is green.
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Rough, green things are quiet.
((("something" "is" "rough" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
If something is green then it is round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
All smart things are kind.
((("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
All rough, smart things are round.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
Quiet, rough things are smart.
((("something" "is" "quiet" "+") ("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
If something is rough and quiet then it is green.
((("something" "is" "rough" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
Gary is big.
True
1
proof
[(triple9)]
("Gary" "is" "big" "+")
triple9
Gary is not green.
False
1
inv-proof
[(triple10)]
("Gary" "is" "green" "-")
triple10
Harry is round.
True
2
proof
[(((triple14) -> rule2))]
("Harry" "is" "round" "+")
((triple14) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Charlie is not kind.
False
2
inv-proof
[(((triple8) -> rule3) OR ((((triple5 triple6) -> rule5)) -> rule3))]
("Charlie" "is" "kind" "-")
((triple8) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple5 triple6) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Bob is not quiet.
Unknown
inv-rconc
[@2: Bob is quiet.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Bob" "is" "quiet" "-")
Bob is green.
Unknown
rconc
[@2: Bob is green.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Bob" "is" "green" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Bob is rough.[(triple1)] Bob is round.[(triple2 OR ((triple1 triple3) -> rule4))] Bob is smart.[(triple3)] Charlie is big.[(triple4)] Charlie is quiet.[(triple5)] Charlie is rough.[(triple6)] Charlie is round.[(triple7 OR ((triple6 triple8) -> rule4) OR ((((triple6 triple5) -> rule6)) -> rule2) OR ((triple6 ((triple5 triple6) -> rule5)) -> rule4))] Charlie is smart.[(triple8 OR ((triple5 triple6) -> rule5))] Gary is big.[(triple9)] Gary is green.[(triple10)] Gary is rough.[(triple11)] Gary is round.[(triple12 OR ((triple10) -> rule2) OR ((triple11 triple13) -> rule4) OR ((triple11 ((((triple11 triple10) -> rule1) triple11) -> rule5)) -> rule4))] Gary is smart.[(triple13 OR ((((triple11 triple10) -> rule1) triple11) -> rule5))] Harry is green.[(triple14)] Harry is quiet.[(triple15)] @1: Bob is kind.[(((triple3) -> rule3))] Charlie is green.[(((triple6 triple5) -> rule6))] Charlie is kind.[(((triple8) -> rule3) OR ((((triple5 triple6) -> rule5)) -> rule3))] Gary is kind.[(((triple13) -> rule3) OR ((((((triple11 triple10) -> rule1) triple11) -> rule5)) -> rule3))] Gary is quiet.[(((triple11 triple10) -> rule1))] Harry is round.[(((triple14) -> rule2))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
((triple1 triple3) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6
Charlie is round.
("Charlie" "is" "round" "+")
triple7
((triple6 triple8) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple6 triple5) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((triple6 ((triple5 triple6) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple8
((triple5 triple6) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
triple9
Gary is green.
("Gary" "is" "green" "+")
triple10
Gary is rough.
("Gary" "is" "rough" "+")
triple11
Gary is round.
("Gary" "is" "round" "+")
triple12
((triple10) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple11 triple13) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple11 ((((triple11 triple10) -> (rule1 % int3)) triple11) -> (rule5 % int2))) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
triple13
((((triple11 triple10) -> (rule1 % int2)) triple11) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
triple14
Harry is quiet.
("Harry" "is" "quiet" "+")
triple15
Bob is kind.
("Bob" "is" "kind" "+")
((triple3) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple6 triple5) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple8) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple5 triple6) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((triple13) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((((triple11 triple10) -> (rule1 % int3)) triple11) -> (rule5 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple11 triple10) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple14) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1