Anne is big. Anne is blue. Anne is kind. Bob is red. Bob is white. Dave is red. Dave is smart. Dave is not white. Fiona is nice. Fiona is smart. If something is big then it is nice. Nice, red things are smart. If something is nice and blue then it is red.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is not white.
("Dave" "is" "white" "-")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
If something is big then it is nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
Nice, red things are smart.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
If something is nice and blue then it is red.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
Dave is not white.
True
1
proof
[(triple8)]
("Dave" "is" "white" "-")
triple8
Dave is white.
False
1
inv-proof
[(triple8)]
("Dave" "is" "white" "+")
triple8
Anne is nice.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not nice.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "nice" "-")
((triple1) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
True
4
proof
[(((((triple1) -> rule1) triple2) -> rule3))]
("Anne" "is" "red" "+")
((((triple1) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not red.
False
4
inv-proof
[(((((triple1) -> rule1) triple2) -> rule3))]
("Anne" "is" "red" "-")
((((triple1) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is smart.
True
7
proof
[(((((triple1) -> rule1) ((((triple1) -> rule1) triple2) -> rule3)) -> rule2))]
("Anne" "is" "smart" "+")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3)) triple2) -> (rule3 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is not smart.
False
7
inv-proof
[(((((triple1) -> rule1) ((((triple1) -> rule1) triple2) -> rule3)) -> rule2))]
("Anne" "is" "smart" "-")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3)) triple2) -> (rule3 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Bob is not smart.
Unknown
inv-rconc
[@2: Bob is smart.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Bob" "is" "smart" "-")
Bob is nice.
Unknown
rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "nice" "+")
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "nice" "-")
Fiona is red.
Unknown
rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "red" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is kind.[(triple3)] Bob is red.[(triple4)] Bob is white.[(triple5)] Dave is not white.[(triple8)] Dave is red.[(triple6)] Dave is smart.[(triple7)] Fiona is nice.[(triple9)] Fiona is smart.[(triple10)] @1: Anne is nice.[(((triple1) -> rule1))] @2: Anne is red.[(((((triple1) -> rule1) triple2) -> rule3))] @3: Anne is smart.[(((((triple1) -> rule1) ((((triple1) -> rule1) triple2) -> rule3)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
Dave is not white.
("Dave" "is" "white" "-")
triple8
Dave is red.
("Dave" "is" "red" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7
Fiona is nice.
("Fiona" "is" "nice" "+")
triple9
Fiona is smart.
("Fiona" "is" "smart" "+")
triple10
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3)) triple2) -> (rule3 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3