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