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