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