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