Bob is red. Erin is white. Fiona is kind. If Bob is young and Bob is red then Bob is nice. All young things are white. All blue things are red. White things are young. If something is red and big then it is young. If something is nice and white then it is young. Kind things are young. All red things are kind.
Bob is red.
("Bob" "is" "red" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
If Bob is young and Bob is red then Bob is nice.
((("Bob" "is" "young" "+") ("Bob" "is" "red" "+")) -> ("Bob" "is" "nice" "+"))
All young things are white.
((("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
All blue things are red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
White things are young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
If something is red and big then it is young.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If something is nice and white then it is young.
((("something" "is" "nice" "+") ("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
Kind things are young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
All red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
Bob is red.
True
1
proof
[(triple1)]
("Bob" "is" "red" "+")
triple1
Fiona is not kind.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "kind" "-")
triple3
Fiona is young.
True
2
proof
[(((triple3) -> rule7))]
("Fiona" "is" "young" "+")
((triple3) -> (rule7 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple1) -> rule8))]
("Bob" "is" "kind" "-")
((triple1) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Fiona is white.
True
3
proof
[(((((triple3) -> rule7)) -> rule2))]
("Fiona" "is" "white" "+")
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Bob is not young.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule7))]
("Bob" "is" "young" "-")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is nice.
True
5
proof
[(((((((triple1) -> rule8)) -> rule7) triple1) -> rule1))]
("Bob" "is" "nice" "+")
((((((triple1) -> (rule8 % int3))) -> (rule7 % int2)) triple1) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is not nice.
False
5
inv-proof
[(((((((triple1) -> rule8)) -> rule7) triple1) -> rule1))]
("Bob" "is" "nice" "-")
((((((triple1) -> (rule8 % int3))) -> (rule7 % int2)) triple1) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "red" "-")
Erin is kind.
Unknown
rconc
[@2: Erin is kind.[CWA. Example of deepest failure = (rule8 <- rule3 <- FAIL)]]
("Erin" "is" "kind" "+")
Fiona is not red.
Unknown
inv-rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "red" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is red.[(triple1)] Erin is white.[(triple2)] Fiona is kind.[(triple3)] @1: Bob is kind.[(((triple1) -> rule8))] Erin is young.[(((triple2) -> rule4))] Fiona is young.[(((triple3) -> rule7))] @2: Bob is young.[(((((triple1) -> rule8)) -> rule7))] Fiona is white.[(((((triple3) -> rule7)) -> rule2))] @3: Bob is nice.[(((((((triple1) -> rule8)) -> rule7) triple1) -> rule1))] Bob is white.[(((((((triple1) -> rule8)) -> rule7)) -> rule2))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Erin is white.
("Erin" "is" "white" "+")
triple2
Fiona is kind.
("Fiona" "is" "kind" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple2) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple3) -> (rule7 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
((((((triple1) -> (rule8 % int3))) -> (rule7 % int2)) triple1) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
((((((triple1) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3