Bob is nice. Charlie is red. Fiona is red. Harry is rough. Nice people are rough. All nice, blue people are cold. If someone is rough then they are blue.
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Nice people are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
All nice, blue people are cold.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
If someone is rough then they are blue.
((("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
Fiona is red.
True
1
proof
[(triple3)]
("Fiona" "is" "red" "+")
triple3
Bob is not nice.
False
1
inv-proof
[(triple1)]
("Bob" "is" "nice" "-")
triple1
Bob is rough.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not rough.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "rough" "-")
((triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("Bob" "is" "blue" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is not blue.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("Bob" "is" "blue" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is cold.
True
5
proof
[(((triple1 ((((triple1) -> rule1)) -> rule3)) -> rule2))]
("Bob" "is" "cold" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is not cold.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule1)) -> rule3)) -> rule2))]
("Bob" "is" "cold" "-")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Fiona is not rough.
Unknown
inv-rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "rough" "-")
Charlie is blue.
Unknown
rconc
[@2: Charlie is blue.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Charlie" "is" "blue" "+")
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "cold" "-")
Fiona is cold.
Unknown
rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "cold" "+")
Fiona is not young.
Unknown
inv-random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Bob is nice.[(triple1)] Charlie is red.[(triple2)] Fiona is red.[(triple3)] Harry is rough.[(triple4)] @1: Bob is rough.[(((triple1) -> rule1))] Harry is blue.[(((triple4) -> rule3))] @2: Bob is blue.[(((((triple1) -> rule1)) -> rule3))] @3: Bob is cold.[(((triple1 ((((triple1) -> rule1)) -> rule3)) -> rule2))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Fiona is red.
("Fiona" "is" "red" "+")
triple3
Harry is rough.
("Harry" "is" "rough" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple4) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3