Bob is big. Charlie is young. Fiona is green. All young people are green. If someone is big then they are green. Green people are nice. All red people are young. If Bob is smart and Bob is green then Bob is big. If someone is smart and green then they are nice.
Bob is big.
("Bob" "is" "big" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is green.
("Fiona" "is" "green" "+")
All young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
If someone is big then they are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
Green people are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
All red people are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If Bob is smart and Bob is green then Bob is big.
((("Bob" "is" "smart" "+") ("Bob" "is" "green" "+")) -> ("Bob" "is" "big" "+"))
If someone is smart and green then they are nice.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Charlie is young.
True
1
proof
[(triple2)]
("Charlie" "is" "young" "+")
triple2
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Charlie is green.
True
2
proof
[(((triple2) -> rule1))]
("Charlie" "is" "green" "+")
((triple2) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Fiona is not nice.
False
2
inv-proof
[(((triple3) -> rule3))]
("Fiona" "is" "nice" "-")
((triple3) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Charlie is nice.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("Charlie" "is" "nice" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Bob is not nice.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("Bob" "is" "nice" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not young.
Unknown
inv-rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "young" "-")
Fiona is young.
Unknown
rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "young" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
@0: Bob is big.[(triple1)] Charlie is young.[(triple2)] Fiona is green.[(triple3)] @1: Bob is green.[(((triple1) -> rule2))] Charlie is green.[(((triple2) -> rule1))] Fiona is nice.[(((triple3) -> rule3))] @2: Bob is nice.[(((((triple1) -> rule2)) -> rule3))] Charlie is nice.[(((((triple2) -> rule1)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Charlie is young.
("Charlie" "is" "young" "+")
triple2
Fiona is green.
("Fiona" "is" "green" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple2) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple3) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2