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