Bob is kind. Bob is red. Bob is young. Erin is red. Erin is young. Gary is red. Gary is young. Harry is nice. Harry is red. Harry is young. If something is quiet and kind then it is nice. All nice things are big. Cold, big things are kind. If Gary is young then Gary is nice. If something is quiet then it is cold. All red things are quiet.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is quiet and kind then it is nice.
((("something" "is" "quiet" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
All nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
Cold, big things are kind.
((("something" "is" "cold" "+") ("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If Gary is young then Gary is nice.
((("Gary" "is" "young" "+")) -> ("Gary" "is" "nice" "+"))
If something is quiet then it is cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
All red things are quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
Gary is young.
True
1
proof
[(triple7)]
("Gary" "is" "young" "+")
triple7
Bob is not red.
False
1
inv-proof
[(triple2)]
("Bob" "is" "red" "-")
triple2
Harry is big.
True
2
proof
[(((triple8) -> rule2))]
("Harry" "is" "big" "+")
((triple8) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple8) -> rule2))]
("Harry" "is" "big" "-")
((triple8) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Bob is cold.
True
3
proof
[(((((triple2) -> rule6)) -> rule5))]
("Bob" "is" "cold" "+")
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not nice.
False
4
inv-proof
[(((((triple2) -> rule6) triple1) -> rule1))]
("Bob" "is" "nice" "-")
((((triple2) -> (rule6 % int2)) triple1) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Gary is kind.
True
7
proof
[(((((((triple6) -> rule6)) -> rule5) ((((triple7) -> rule4)) -> rule2)) -> rule3))]
("Gary" "is" "kind" "+")
((((((triple6) -> (rule6 % int5))) -> (rule5 % int4)) ((((triple7) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
int5
Gary is not kind.
False
7
inv-proof
[(((((((triple6) -> rule6)) -> rule5) ((((triple7) -> rule4)) -> rule2)) -> rule3))]
("Gary" "is" "kind" "-")
((((((triple6) -> (rule6 % int5))) -> (rule5 % int4)) ((((triple7) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
int5
Erin is not big.
Unknown
inv-rconc
[@3: Erin is big.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule3 <- FAIL)]]
("Erin" "is" "big" "-")
Erin is nice.
Unknown
rconc
[@3: Erin is nice.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule2 <- FAIL)]]
("Erin" "is" "nice" "+")
@0: Bob is kind.[(triple1)] Bob is red.[(triple2)] Bob is young.[(triple3)] Erin is red.[(triple4)] Erin is young.[(triple5)] Gary is red.[(triple6)] Gary is young.[(triple7)] Harry is nice.[(triple8)] Harry is red.[(triple9)] Harry is young.[(triple10)] @1: Bob is quiet.[(((triple2) -> rule6))] Erin is quiet.[(((triple4) -> rule6))] Gary is nice.[(((triple7) -> rule4))] Gary is quiet.[(((triple6) -> rule6))] Harry is big.[(((triple8) -> rule2))] Harry is quiet.[(((triple9) -> rule6))] @2: Bob is cold.[(((((triple2) -> rule6)) -> rule5))] Bob is nice.[(((((triple2) -> rule6) triple1) -> rule1))] Erin is cold.[(((((triple4) -> rule6)) -> rule5))] Gary is big.[(((((triple7) -> rule4)) -> rule2))] Gary is cold.[(((((triple6) -> rule6)) -> rule5))] Harry is cold.[(((((triple9) -> rule6)) -> rule5))] @3: Bob is big.[(((((((triple2) -> rule6) triple1) -> rule1)) -> rule2))] Gary is kind.[(((((((triple6) -> rule6)) -> rule5) ((((triple7) -> rule4)) -> rule2)) -> rule3))] Harry is kind.[(((((((triple9) -> rule6)) -> rule5) ((triple8) -> rule2)) -> rule3))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Erin is red.
("Erin" "is" "red" "+")
triple4
Erin is young.
("Erin" "is" "young" "+")
triple5
Gary is red.
("Gary" "is" "red" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Harry is nice.
("Harry" "is" "nice" "+")
triple8
Harry is red.
("Harry" "is" "red" "+")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple2) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple4) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple7) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple6) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple8) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple9) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
((((triple2) -> (rule6 % int2)) triple1) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((((triple4) -> (rule6 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((((triple7) -> (rule4 % int2))) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((triple6) -> (rule6 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((((triple9) -> (rule6 % int2))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
((((((triple2) -> (rule6 % int3)) triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
((((((triple6) -> (rule6 % int5))) -> (rule5 % int4)) ((((triple7) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
int5
Harry is kind.
("Harry" "is" "kind" "+")
((((((triple9) -> (rule6 % int4))) -> (rule5 % int3)) ((triple8) -> (rule2 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4