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