Bob is blue. Bob is green. Charlie is blue. Charlie is round. Fiona is nice. Harry is kind. Harry is round. Round, kind people are nice. If someone is green then they are cold. If someone is nice then they are green.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
Round, kind people are nice.
((("someone" "is" "round" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
If someone is green then they are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
If someone is nice then they are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
Fiona is nice.
True
1
proof
[(triple5)]
("Fiona" "is" "nice" "+")
triple5
Fiona is not nice.
False
1
inv-proof
[(triple5)]
("Fiona" "is" "nice" "-")
triple5
Fiona is green.
True
2
proof
[(((triple5) -> rule3))]
("Fiona" "is" "green" "+")
((triple5) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Bob is not cold.
False
2
inv-proof
[(((triple2) -> rule2))]
("Bob" "is" "cold" "-")
((triple2) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Harry is green.
True
4
proof
[(((((triple7 triple6) -> rule1)) -> rule3))]
("Harry" "is" "green" "+")
((((triple7 triple6) -> (rule1 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Fiona is not cold.
False
3
inv-proof
[(((((triple5) -> rule3)) -> rule2))]
("Fiona" "is" "cold" "-")
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Harry is cold.
True
5
proof
[(((((((triple7 triple6) -> rule1)) -> rule3)) -> rule2))]
("Harry" "is" "cold" "+")
((((((triple7 triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is not cold.
False
5
inv-proof
[(((((((triple7 triple6) -> rule1)) -> rule3)) -> rule2))]
("Harry" "is" "cold" "-")
((((((triple7 triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Charlie is not cold.
Unknown
inv-rconc
[@3: Charlie is cold.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule1 <- FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is nice.
Unknown
rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "nice" "+")
Charlie is not green.
Unknown
inv-rconc
[@2: Charlie is green.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Charlie" "is" "green" "-")
Bob is nice.
Unknown
rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "nice" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
@0: Bob is blue.[(triple1)] Bob is green.[(triple2)] Charlie is blue.[(triple3)] Charlie is round.[(triple4)] Fiona is nice.[(triple5)] Harry is kind.[(triple6)] Harry is round.[(triple7)] @1: Bob is cold.[(((triple2) -> rule2))] Fiona is green.[(((triple5) -> rule3))] Harry is nice.[(((triple7 triple6) -> rule1))] @2: Fiona is cold.[(((((triple5) -> rule3)) -> rule2))] Harry is green.[(((((triple7 triple6) -> rule1)) -> rule3))] @3: Harry is cold.[(((((((triple7 triple6) -> rule1)) -> rule3)) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
triple4
Fiona is nice.
("Fiona" "is" "nice" "+")
triple5
Harry is kind.
("Harry" "is" "kind" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
Bob is cold.
("Bob" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple5) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple7 triple6) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((((triple7 triple6) -> (rule1 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((((((triple7 triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3