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