Bob is red. Dave is smart. Fiona is rough. Blue, rough things are red. All blue, rough things are cold. All young things are smart. If something is blue then it is rough. If something is smart then it is blue. If Bob is cold and Bob is smart then Bob is rough. All smart, kind things are rough. If something is rough and blue then it is red.
Bob is red.
("Bob" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Blue, rough things are red.
((("something" "is" "blue" "+") ("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
All blue, rough things are cold.
((("something" "is" "blue" "+") ("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
All young things are smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
If something is blue then it is rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If something is smart then it is blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
If Bob is cold and Bob is smart then Bob is rough.
((("Bob" "is" "cold" "+") ("Bob" "is" "smart" "+")) -> ("Bob" "is" "rough" "+"))
All smart, kind things are rough.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something is rough and blue then it is red.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
Bob is red.
True
1
proof
[(triple1)]
("Bob" "is" "red" "+")
triple1
Dave is not smart.
False
1
inv-proof
[(triple2)]
("Dave" "is" "smart" "-")
triple2
Dave is blue.
True
2
proof
[(((triple2) -> rule5))]
("Dave" "is" "blue" "+")
((triple2) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple2) -> rule5))]
("Dave" "is" "blue" "-")
((triple2) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
True
3
proof
[(((((triple2) -> rule5)) -> rule4))]
("Dave" "is" "rough" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not rough.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule4))]
("Dave" "is" "rough" "-")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is cold.
True
6
proof
[(((((triple2) -> rule5) ((((triple2) -> rule5)) -> rule4)) -> rule2))]
("Dave" "is" "cold" "+")
((((triple2) -> (rule5 % int3)) ((((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is not cold.
False
6
inv-proof
[(((((triple2) -> rule5) ((((triple2) -> rule5)) -> rule4)) -> rule2))]
("Dave" "is" "cold" "-")
((((triple2) -> (rule5 % int3)) ((((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Bob is not rough.
Unknown
inv-rconc
[@3: Bob is rough.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule3 <- FAIL)]]
("Bob" "is" "rough" "-")
Fiona is cold.
Unknown
rconc
[@3: Fiona is cold.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule3 <- FAIL)]]
("Fiona" "is" "cold" "+")
Fiona is not blue.
Unknown
inv-rconc
[@2: Fiona is blue.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is red.
Unknown
rconc
[@3: Fiona is red.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule3 <- FAIL)]]
("Fiona" "is" "red" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
@0: Bob is red.[(triple1)] Dave is smart.[(triple2)] Fiona is rough.[(triple3)] @1: Dave is blue.[(((triple2) -> rule5))] @2: Dave is rough.[(((((triple2) -> rule5)) -> rule4))] @3: Dave is cold.[(((((triple2) -> rule5) ((((triple2) -> rule5)) -> rule4)) -> rule2))] Dave is red.[(((((triple2) -> rule5) ((((triple2) -> rule5)) -> rule4)) -> rule1) OR ((((((triple2) -> rule5)) -> rule4) ((triple2) -> rule5)) -> rule8))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Fiona is rough.
("Fiona" "is" "rough" "+")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
((triple2) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((((triple2) -> (rule5 % int3)) ((((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
((((triple2) -> (rule5 % int3)) ((((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((((((triple2) -> (rule5 % int3))) -> (rule4 % int2)) ((triple2) -> (rule5 % int3))) -> (rule8 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3