Charlie is not green. Charlie is not red. Dave is big. Dave is green. Dave is nice. Dave is red. Dave is rough. Dave is smart. Dave is young. Fiona is big. Fiona is green. Fiona is not rough. If someone is red and not young then they are not green. All green, red people are rough. Big people are smart. All big, smart people are nice. If someone is rough and not green then they are nice. All red, big people are nice.
Charlie is not green.
("Charlie" "is" "green" "-")
Charlie is not red.
("Charlie" "is" "red" "-")
Dave is big.
("Dave" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is not rough.
("Fiona" "is" "rough" "-")
If someone is red and not young then they are not green.
((("someone" "is" "red" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "green" "-"))
All green, red people are rough.
((("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
Big people are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
All big, smart people are nice.
((("someone" "is" "big" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
If someone is rough and not green then they are nice.
((("someone" "is" "rough" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "nice" "+"))
All red, big people are nice.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
Fiona is green.
True
1
proof
[(triple11)]
("Fiona" "is" "green" "+")
triple11
Dave is not nice.
False
1
inv-proof
[(triple5 OR ((triple3 triple8) -> rule4) OR ((triple6 triple3) -> rule6) OR ((triple3 ((triple3) -> rule3)) -> rule4))]
("Dave" "is" "nice" "-")
triple5
((triple3 triple8) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple6 triple3) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple3 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Fiona is smart.
True
2
proof
[(((triple10) -> rule3))]
("Fiona" "is" "smart" "+")
((triple10) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is not smart.
False
2
inv-proof
[(((triple10) -> rule3))]
("Fiona" "is" "smart" "-")
((triple10) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is nice.
True
4
proof
[(((triple10 ((triple10) -> rule3)) -> rule4))]
("Fiona" "is" "nice" "+")
((triple10 ((triple10) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is not nice.
False
4
inv-proof
[(((triple10 ((triple10) -> rule3)) -> rule4))]
("Fiona" "is" "nice" "-")
((triple10 ((triple10) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is nice.
Unknown
rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "nice" "+")
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "smart" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Charlie is not green.[(triple1)] Charlie is not red.[(triple2)] Dave is big.[(triple3)] Dave is green.[(triple4)] Dave is nice.[(triple5 OR ((triple3 triple8) -> rule4) OR ((triple6 triple3) -> rule6) OR ((triple3 ((triple3) -> rule3)) -> rule4))] Dave is red.[(triple6)] Dave is rough.[(triple7 OR ((triple4 triple6) -> rule2))] Dave is smart.[(triple8 OR ((triple3) -> rule3))] Dave is young.[(triple9)] Fiona is big.[(triple10)] Fiona is green.[(triple11)] Fiona is not rough.[(triple12)] @1: Fiona is smart.[(((triple10) -> rule3))] @2: Fiona is nice.[(((triple10 ((triple10) -> rule3)) -> rule4))]
Charlie is not green.
("Charlie" "is" "green" "-")
triple1
Charlie is not red.
("Charlie" "is" "red" "-")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
triple4
Dave is nice.
("Dave" "is" "nice" "+")
triple5
((triple3 triple8) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple6 triple3) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple3 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple6
Dave is rough.
("Dave" "is" "rough" "+")
triple7
((triple4 triple6) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple8
((triple3) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple9
Fiona is big.
("Fiona" "is" "big" "+")
triple10
Fiona is green.
("Fiona" "is" "green" "+")
triple11
Fiona is not rough.
("Fiona" "is" "rough" "-")
triple12
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple10) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple10 ((triple10) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2