Bob is young. Dave is green. Fiona is round. If something is young then it is cold. Cold things are nice. If something is green and nice then it is young. If Bob is red and Bob is cold then Bob is nice. All red things are green. All young, nice things are red.
Bob is young.
("Bob" "is" "young" "+")
Dave is green.
("Dave" "is" "green" "+")
Fiona is round.
("Fiona" "is" "round" "+")
If something is young then it is cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
Cold things are nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If something is green and nice then it is young.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If Bob is red and Bob is cold then Bob is nice.
((("Bob" "is" "red" "+") ("Bob" "is" "cold" "+")) -> ("Bob" "is" "nice" "+"))
All red things are green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
All young, nice things are red.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
Fiona is round.
True
1
proof
[(triple3)]
("Fiona" "is" "round" "+")
triple3
Dave is not green.
False
1
inv-proof
[(triple2)]
("Dave" "is" "green" "-")
triple2
Bob is cold.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is not cold.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "cold" "-")
((triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is nice.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("Bob" "is" "nice" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not nice.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("Bob" "is" "nice" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is red.
True
5
proof
[(((triple1 ((((triple1) -> rule1)) -> rule2)) -> rule6))]
("Bob" "is" "red" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is not red.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule1)) -> rule2)) -> rule6))]
("Bob" "is" "red" "-")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Dave is not red.
Unknown
inv-rconc
[@4: Dave is red.[CWA. Example of deepest failure = (rule6 <- rule3 <- rule2 <- rule1 <- FAIL)]]
("Dave" "is" "red" "-")
Dave is cold.
Unknown
rconc
[@3: Dave is cold.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule2 <- FAIL)]]
("Dave" "is" "cold" "+")
Fiona is not nice.
Unknown
inv-rconc
[@3: Fiona is nice.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule3 <- FAIL)]]
("Fiona" "is" "nice" "-")
Dave is young.
Unknown
rconc
[@3: Dave is young.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule1 <- FAIL)]]
("Dave" "is" "young" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Bob is young.[(triple1)] Dave is green.[(triple2)] Fiona is round.[(triple3)] @1: Bob is cold.[(((triple1) -> rule1))] @2: Bob is nice.[(((((triple1) -> rule1)) -> rule2))] @3: Bob is red.[(((triple1 ((((triple1) -> rule1)) -> rule2)) -> rule6))] @4: Bob is green.[(((((triple1 ((((triple1) -> rule1)) -> rule2)) -> rule6)) -> rule5))]
Bob is young.
("Bob" "is" "young" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Fiona is round.
("Fiona" "is" "round" "+")
triple3
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
((((triple1 ((((triple1) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4