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