Bob is nice. Bob is quiet. Bob is rough. Bob is smart. Charlie is furry. Charlie is nice. Charlie is rough. Charlie is smart. Fiona is big. Fiona is quiet. Fiona is round. Fiona is smart. Gary is furry. Gary is quiet. Gary is round. Gary is smart. If someone is smart and furry then they are quiet. If Fiona is rough then Fiona is big. If Bob is big and Bob is nice then Bob is quiet. Round people are rough. All round, big people are smart. All round, rough people are nice. All big people are smart. Furry, quiet people are rough.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If someone is smart and furry then they are quiet.
((("someone" "is" "smart" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If Fiona is rough then Fiona is big.
((("Fiona" "is" "rough" "+")) -> ("Fiona" "is" "big" "+"))
If Bob is big and Bob is nice then Bob is quiet.
((("Bob" "is" "big" "+") ("Bob" "is" "nice" "+")) -> ("Bob" "is" "quiet" "+"))
Round people are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
All round, big people are smart.
((("someone" "is" "round" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
All round, rough people are nice.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
All big people are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
Furry, quiet people are rough.
((("someone" "is" "furry" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
Fiona is smart.
True
1
proof
[(triple12 OR ((triple9) -> rule7) OR ((triple11 triple9) -> rule5) OR ((((((triple11) -> rule4)) -> rule2)) -> rule7) OR ((triple11 ((((triple11) -> rule4)) -> rule2)) -> rule5))]
("Fiona" "is" "smart" "+")
triple12
((triple9) -> (rule7 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple11 triple9) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((((triple11) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
((triple11 ((((triple11) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Charlie is not smart.
False
1
inv-proof
[(triple8)]
("Charlie" "is" "smart" "-")
triple8
Charlie is quiet.
True
3
proof
[(((triple8 triple5) -> rule1))]
("Charlie" "is" "quiet" "+")
((triple8 triple5) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not quiet.
False
3
inv-proof
[(((triple8 triple5) -> rule1))]
("Charlie" "is" "quiet" "-")
((triple8 triple5) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Bob is nice.[(triple1)] Bob is quiet.[(triple2)] Bob is rough.[(triple3)] Bob is smart.[(triple4)] Charlie is furry.[(triple5)] Charlie is nice.[(triple6)] Charlie is rough.[(triple7 OR ((triple5 ((triple8 triple5) -> rule1)) -> rule8))] Charlie is smart.[(triple8)] Fiona is big.[(triple9 OR ((((triple11) -> rule4)) -> rule2))] Fiona is quiet.[(triple10)] Fiona is round.[(triple11)] Fiona is smart.[(triple12 OR ((triple9) -> rule7) OR ((triple11 triple9) -> rule5) OR ((((((triple11) -> rule4)) -> rule2)) -> rule7) OR ((triple11 ((((triple11) -> rule4)) -> rule2)) -> rule5))] Gary is furry.[(triple13)] Gary is quiet.[(triple14 OR ((triple16 triple13) -> rule1))] Gary is round.[(triple15)] Gary is smart.[(triple16)] @1: Charlie is quiet.[(((triple8 triple5) -> rule1))] Fiona is rough.[(((triple11) -> rule4))] Gary is rough.[(((triple15) -> rule4) OR ((triple13 triple14) -> rule8) OR ((triple13 ((triple16 triple13) -> rule1)) -> rule8))] @2: Fiona is nice.[(((triple11 ((triple11) -> rule4)) -> rule6))] Gary is nice.[(((triple15 ((triple15) -> rule4)) -> rule6) OR ((triple15 ((triple13 triple14) -> rule8)) -> rule6) OR ((triple15 ((triple13 ((triple16 triple13) -> rule1)) -> rule8)) -> rule6))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Charlie is furry.
("Charlie" "is" "furry" "+")
triple5
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
Charlie is rough.
("Charlie" "is" "rough" "+")
triple7
((triple5 ((triple8 triple5) -> (rule1 % int2))) -> (rule8 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple8
Fiona is big.
("Fiona" "is" "big" "+")
triple9
((((triple11) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple10
Fiona is round.
("Fiona" "is" "round" "+")
triple11
Fiona is smart.
("Fiona" "is" "smart" "+")
triple12
((triple9) -> (rule7 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple11 triple9) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((((triple11) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
((triple11 ((((triple11) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
triple13
Gary is quiet.
("Gary" "is" "quiet" "+")
triple14
((triple16 triple13) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
triple15
Gary is smart.
("Gary" "is" "smart" "+")
triple16
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple8 triple5) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple11) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple15) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple13 triple14) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple13 ((triple16 triple13) -> (rule1 % int2))) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple11 ((triple11) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((triple15 ((triple15) -> (rule4 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((triple15 ((triple13 triple14) -> (rule8 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((triple15 ((triple13 ((triple16 triple13) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3